package naruto.dynamicanalysis.tracing;

import naruto.datastructures.trace.*;
import naruto.datastructures.criteria.*;
import gov.nasa.jpf.*;
import gov.nasa.jpf.jvm.*;
import gov.nasa.jpf.jvm.bytecode.InvokeInstruction;
import gov.nasa.jpf.jvm.bytecode.ReturnInstruction;
import java.util.*;
import naruto.common.*;
import naruto.datastructures.instruction.*;

/**
 *
 * @author nacuong
 */
public class IfCompleteTracer extends ListenerAdapter {
  /* the set contains method elements to be captured during tracing */
  Vector<Criteria> criteriaSet;
  /* the stack to store partial if complete trace */
  Vector<Stack<IfCompleteTrace>> traceStackSet;
  /* the hashtable to capture recursive call for each method */
  Hashtable<String, Integer> recursiveCounter;

  public IfCompleteTracer(Vector<Criteria> criteriaSet) {
    this.criteriaSet = criteriaSet;
    this.traceStackSet = new Vector<Stack<IfCompleteTrace>>();
    for (int i = 0; i < criteriaSet.size(); i++) {
      traceStackSet.add(new Stack<IfCompleteTrace>());
    }
    recursiveCounter = new Hashtable<String, Integer>();
  }

  /**
	* This run method provides a direct application of IfCompleteTracer class. Given a program and its corresponding
	* test input, "run" extracts during runtime a set of if-complete trace which is coressponding with a set
	* of provided criterion.
	* @param	args	jpf execution arguments, it includes a java class file and its corresponding input
	* @return	a vector of if-complete trace which is corresponding with a set of provided criterion
	*/
  public Vector<IfCompleteTrace> run(String[] args) {
    Config conf = JPF.createConfig(args);
    JPF jpf = new JPF(conf);
    jpf.addListener(this);
    jpf.run();

    Vector<IfCompleteTrace> traceSet = new Vector<IfCompleteTrace>();
    
    for (Stack<IfCompleteTrace> traceStack : traceStackSet)
      if (traceStack.size() != 1)
        System.err.println("err!");
      else
        traceSet.add(traceStack.pop());
    
    return traceSet;
  }

  @Override
  public void instructionExecuted(JVM vm) {
    gov.nasa.jpf.jvm.bytecode.Instruction insn = vm.getLastInstruction();
    if (isDesirableInstruction(insn)) {      
      /* compute method call recursive counter */
      computeRecursiveCounter(insn);

      /* produce ifcomplete trace for each critera */
      for (int inx = 0; inx < criteriaSet.size(); inx++) {
        Criteria criteria = criteriaSet.get(inx);
        Stack<IfCompleteTrace> traceStack = traceStackSet.get(inx);
        /* initialize traceStack if neccessary */
        if (traceStack.isEmpty())
          traceStack.push(new IfCompleteTrace());
        
        /* put in endif instruction */
        if (traceStack.size() > 1) {
          /* if instruction is always at the beginning of a frame (except the first frame) */
          gov.nasa.jpf.jvm.bytecode.IfInstruction ifInsn =
                  (gov.nasa.jpf.jvm.bytecode.IfInstruction) traceStack.peek().get(0).getInstruction();
          while (InstructionCommon.isEndIfInstruction(insn,ifInsn,recursiveCounter)){
            traceEndIfInstruction(ifInsn,traceStack, criteria);
            if (traceStack.size() > 1)
              ifInsn = (gov.nasa.jpf.jvm.bytecode.IfInstruction) traceStack.peek().get(0).getInstruction();
            else
              break;
          }
        }

        /* put in if instruction */
        if (InstructionCommon.isIfInstruction(insn)){
          traceIfInstruction((gov.nasa.jpf.jvm.bytecode.IfInstruction)insn, traceStack, criteria);
        }
        /* put in method instruction */
        if (InstructionCommon.isMethodCall(insn))
          traceMethodInstruction((InvokeInstruction)insn, traceStack, criteria);
      }
    }
  }

  /**
   * Tracing an endif isntruction. This endif instruction close a complete if-complete segment.
   * The endif isntruction is traced only when the complete if-segment contains some criteria.
   * 
   * @param endIfInstruction
   * @param traceStack
   * @param criteria
   */
  private void traceEndIfInstruction(gov.nasa.jpf.jvm.bytecode.IfInstruction endIfInstruction, Stack<IfCompleteTrace> traceStack, Criteria criteria){
    IfCompleteTrace ifCompleteTrace = traceStack.pop();
    ifCompleteTrace.add(new EndIfInstruction(endIfInstruction, getRecursiveCounter(endIfInstruction)));
    if (ifCompleteTrace.containCriteria(criteria))
      traceStack.peek().addAll(ifCompleteTrace);
  }

  /**
   * Tracing an if instruction. An if instruction is always put in a new stack frame.
   * @param ifInstruction
   * @param traceStack
   */
  private void traceIfInstruction(gov.nasa.jpf.jvm.bytecode.IfInstruction ifInstruction, Stack<IfCompleteTrace> traceStack, Criteria criteria) {
    traceStack.push(new IfCompleteTrace());
//    System.out.println(ifInstruction.getSourceLine() + " " + ifInstruction.getConditionValue());
          
    IfInstruction ifInsn = new IfInstruction(ifInstruction, getRecursiveCounter(ifInstruction));
    traceStack.peek().add(ifInsn);

    if (isDesirableIfInstruction(ifInstruction)){
      InstructionCriterion instructionCriterion =
              new InstructionCriterion(ifInsn.getClassName(),ifInsn.getMethodInfoName(), ifInsn.getOffset());
      if (!criteria.contains(instructionCriterion))
        criteria.add(instructionCriterion);
    }
  }

  /**
   * Tracing a method instruction. The method is traced only if it belongs to the criteria.
   * @param methodInstruction
   * @param traceStack
   */
  private void traceMethodInstruction(InvokeInstruction methodInstruction, Stack<IfCompleteTrace> traceStack, Criteria criteria){
    MethodInstruction methodInsn = new MethodInstruction(methodInstruction);
    MethodCallCriterion methodCallCriterion = new MethodCallCriterion(methodInsn.getMethodName());
    
    if (criteria.contains(methodCallCriterion))
      traceStack.peek().add(new MethodInstruction(methodInstruction, getRecursiveCounter(methodInstruction)));
  }

  public static boolean contains(Vector<Criterion> criteria, MethodCallCriterion methodCallCriterion){
    for (Criterion criterion: criteria){
      if (methodCallCriterion.equals(criterion))
        return true;
    }
    return false;
  }

  /**
   * Get recursive counter of the method that the instruction belongs to.
   * @param instruction
   * @return
   */
  public int getRecursiveCounter(gov.nasa.jpf.jvm.bytecode.Instruction instruction){
    String methodInfoName = instruction.getMethodInfo().getCompleteName();
    if (recursiveCounter.containsKey(methodInfoName))
      return recursiveCounter.get(methodInfoName);
    else
      return 1;
  }

  /**
   * Compute method recursive counter information for each new instruction received.
   * If instruction is a new method call, update recursiveCounter hashtable with this
   * instruction and the counter 1.
   * If instruction is an old method call, increase the method call counter by 1.
   * If instruction is a return statement, decrease the counter of method that contains this instruction by 1.
   * 
   * @param insn  the new instruction that is received.
   */
  private void computeRecursiveCounter(gov.nasa.jpf.jvm.bytecode.Instruction insn) {
    if (insn instanceof InvokeInstruction) {
      String methodName = ((InvokeInstruction) insn).getInvokedMethod().getCompleteName();
      if (!recursiveCounter.containsKey(methodName)) {
        recursiveCounter.put(methodName, 1);         /* put new method call in hashtable */
      } else {
        int counter = recursiveCounter.get(methodName);
        recursiveCounter.put(methodName, counter + 1); /* increase counter of a recursive method */
      }
    }

    if (insn instanceof ReturnInstruction) {
      String methodInfoName = insn.getMethodInfo().getCompleteName();
      if (recursiveCounter.containsKey(methodInfoName)) {
        int counter = recursiveCounter.get(methodInfoName);
        recursiveCounter.put(methodInfoName, counter + 1); /* decrease counter of a recursive method */
      }
    }
  }

  /**
   * Determine whether this instruction should be traced into the ifcomplete tracer.
   * Currently, only library instruction are not traced.
   *
   * @param insn the instruction that is considered
   * @return true if the instruction should be traced; false otherwise
   */
  private boolean isDesirableInstruction(gov.nasa.jpf.jvm.bytecode.Instruction insn) {
    return !InstructionCommon.isLibraryInstruction(insn);
  }

  /**
   * This method choose some desirable if to keep as a criterion.
   * @param insn
   * @return
   */
  private boolean isDesirableIfInstruction(gov.nasa.jpf.jvm.bytecode.IfInstruction insn){
    // TODO implement this
    return false;
  }
}
